
\emph{Session types} 
offer a powerful type-theoretic foundation  
for the analysis of 
complex scenarios of structured communications, as frequently found in service-oriented systems.  
They abstract communication protocols as basic interaction patterns, which 
are then statically checked against specifications
in some core programming calculus---typ\-i\-cal\-ly, a variant of the $\pi$-calculus~\cite{DBLP:journals/iandc/MilnerPW92a}. 
Introduced in~\cite{DBLP:conf/concur/Honda93,DBLP:conf/esop/HondaVK98}, 
session type theories 
%have received much attention and 
have been extended in many directions---see~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a survey. 
Their practical relevance %of session types 
is witnessed by, e.g., 
 their recent application in the verification of parallel systems~\cite{DBLP:conf/tools/NgYH12}.

In spite of these developments, 
we find that existing ses\-sion-typed
calculi do not explicitly support 
%for reasoning about 
mechanisms for 
\emph{runtime adaptation}. 
While channel mobility (also known as \emph{delegation}~\cite{DBLP:journals/entcs/YoshidaV07}) 
as supported by such calculi
is often useful to model forms of
dynamic reconfiguration, more general forms of adaptation/evolvability 
are not expressible or are hard to reason about.
%Adaptation and evolvability are increasingly relevant issues nowadays, 
Runtime adaptation is an increasingly relevant issue nowadays, 
as distributed systems and applications are  being deployed in
open, highly dynamic infrastructures, such as cloud computing platforms.
In such settings,  
runtime adaptation %and dynamic reconfiguration  
appears as a key feature to
ensure continued system operation,
reduce costs, and achieve
business agility. 

We thus observe a rather unfortunate discrepancy between 
(i)~the evolvability capabilities of modern communicating systems in practice, and 
(ii)~the forms of interaction available in 
%the calculi upon which session types disciplines are defined.
(typed) process frameworks developed to reason about the correctness of such systems.


In this paper, we propose a simple approach towards overcoming this discrepancy.
We %extend an existing 
introduce a
session types discipline 
for a language
equipped
with 
mechanisms for runtime adaptation.
Rather than developing yet another session types discipline \emph{from scratch}, we have deliberately 
preferred to build upon existing lines of work. 
Our proposal 
builds upon
%results from combining 
the framework of 
\emph{adaptable processes}, 
an attempt for enhancing process calculi specifications with evolvability mechanisms
which we have developed together with Bravetti and Zavattaro in~\cite{BGPZFMOODS}.
We combine the constructs for adaptable processes with
the main insights %principles %underlying the discipline 
of the session type system
put forward by Garralda et al.~\cite{DBLP:conf/ppdp/GarraldaCD06} for the Boxed Ambient calculus~\cite{DBLP:journals/toplas/BugliesiCC04}.
Since the type system in~\cite{DBLP:conf/ppdp/GarraldaCD06} does not handle delegation, 
we  support this important mechanism by relying on the ``liberal'' typing system described in~\cite{DBLP:journals/entcs/YoshidaV07}.
As a result of this integration of concepts, 
we obtain a simple yet expressive model 
of structured communications with explicit mechanisms for runtime adaptation.


We briefly describe our approach and results. 
Our process language includes
the usual $\pi$-calculus constructs for session communication, but extended 
with the \emph{located processes} and the \emph{update processes} introduced in~\cite{BGPZFMOODS}.
Given a location $l$, a process $P$, and a context $Q(\mathsf{X})$ 
(i.e. a process $Q$ with free occurrences of variable $\mathsf{X}$), these processes are noted $l[P]$ and 
$\adapt{l}{Q}{X}$, respectively. 
%$l\{Q(\mathsf{X})\}$, resp. 
They may synchronize on $l$ so as to evolve into process 
$Q\subst{P}{\mathsf{X}}$ ---the process $Q$ in which all free occurrences of $X$ are replaced with $P$.
This interaction represents the \emph{update} of  process $P$ at $l$ with an \emph{adaptation routine}
(or built-in adaptation mechanism)
embodied by $Q(\mathsf{X})$. Locations can be nested and are transparent:
within $l[P]$, process $P$ may evolve autonomously, with the potential of interacting with some neighboring 
update process for $l$. 
%$l\{Q(\mathsf{X})\}$, 
%$\adapt{l}{Q}{X}$,
%as just described, 
Hence, 
in our language communicating behavior coexists with update actions. 
This raises the need for disciplining both forms of interaction, in such a way that 
 session types descriptions are respected and  evolvability requirements are enforced. 
To this end, by observing that %exploiting the fact that 
our update actions are a simple form of (higher-order) process mobility, 
we draw inspiration from the session types 
in~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
which ensure that
sessions within Ambient hierarchies %are \emph{safe}, i.e., they 
are never disrupted by Ambient mobility steps.
By generalizing this insight to the context of (session) processes which execute
in arbitrary, possibly nested locations, we obtain a property which we call \emph{consistency}:
update actions over located processes which are engaged in active session behavior cannot be enabled.

%While both Ambients and adaptable processes rely on nested located processes,
%Ambient mobility and evolvability steps are conceptually very different.
%In fact, %is a major difference:
%Ambient mobility is only defined in a parent-child style, whereas
%located processes and update actions 
% may interact independently of their relative position in the hierarchy induced by location nesting.
%This way, integrating our calculus for adaptable processes %of~\cite{BGPZFMOODS} 
%with the session types discipline in~\cite{DBLP:conf/ppdp/GarraldaCD06}
%roughly amounts to: 

To show how
located and update processes fit in a session-typed process language, 
and to illustrate our  notion of consistency, 
we  consider a simple distributed client/server scenario,
% of distributed, interacting services (a client $C_1$ and a replicated service $S$), 
conveniently represented as located processes:
\begin{eqnarray*}
\mathsf{Sys} & \triangleq &  %\scomponent{l_{0}}{C_1} \para 
\scomponent{l_{1}}{C_1} \para\bigscomponent{l_2}{\scomponent{r}{S} \para R \, } \quad\text{where:} \vspace{3mm} \\ 
C_1  &  \triangleq  & \nopenr{a}{x}.\outC{x}{u_1,p_1}.\select{x}{n_1.P_1}.\close{x} \\
S  &  \triangleq  & \repopen{a}{y}.\inC{y}{u,p}.\branch{y}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{y} 
\end{eqnarray*}
Intuitively, 
$\mathsf{Sys}$ 
consists of a replicated server $S$ and a client $C_1$, hosted in different locations $l_1$ and $r$.
They 
may  establish a session %of type $\sigma$ 
%between $S$ and $C_1$ %($i \in \{0, 1\}$) 
using name $a$:
first, the client sends its credentials to the server; then, the client chooses one of the 
services offered by the server. 
Above, the actual client and server behaviors are  abstracted by processes $P_1$ and $Q_1$, respectively.
%(resp. $P_1$ and $Q_1$), 
%which are left unspecified.
Finally, server and client synchronize to close the session.
Process  $R$, in location $l_2$, represents the platform in which  $S$ is deployed.

Starting from $\mathsf{Sys}$, let us suppose that a new session is indeed established by synchronization on $a$. 
Our semantics decrees the following reduction step:  %We then have
\begin{eqnarray*}
\mathsf{Sys} \!\!\!& \pired & \!\!\!\! (\nu \kappa)\big(\scomponent{l_{1}}{\outC{\kappa^{+}}{u_1,p_1}.\select{\kappa^{+}}{n_1.P_1}.\close{\kappa^{+}}} \para \\ 
& & \quad \bigscomponent{l_2}{\scomponent{r}{\inC{\kappa^{-}}{u,p}.\branch{\kappa^{-}}{n_1{:}Q_1 \parallel n_2{:}Q_2}.\close{\kappa^{-}} \para S\,} \para R \, }\big) = \mathsf{Sys}'
\end{eqnarray*} 
where 
$\kappa^+$ and $\kappa^-$ denote the two \emph{end-points} of channel $\kappa$~\cite{DBLP:journals/acta/GayH05}.
Suppose now that $R$ simply represents an upgrade process, which is ready to synchronize with $r$, the location in which $S$ resides: 
$$R = \adaptn{r}{NewS(\mathsf{X})}$$
From $\mathsf{Sys}'$, an update on $r$ would be  inconvenient for at least two reasons:
\begin{enumerate}[(a)]
\item First, since $r$ contains the local server behavior for an already established session, 
a careless update action on $r$ could potentially discard such behavior. This would leave the client in $l_1$ without a partner---the  protocol agreed upon session establishment would not be respected. 
\item Second, since $r$ contains also the actual service definition $S$, an undisciplined 
update action on $r$ could 
affect the service on $a$ in a variety of ways---for instance, it could destroy it. 
This clearly goes against the expected nature of services, which should be always available. 
\end{enumerate}

Above, item (a) concerns our intended notion of consistency, which ensures that any update actions on $r$
(such as those involving $R$ above) are only enabled  when $r$ contains no active sessions. 
Closely related, item (b) concerns a most desirable principle for services, namely that ``services should always be available in multiple copies''---this is the Service Channel Principle (SCP) identified in~\cite{DBLP:conf/esop/CarboneHY07}.


\paragraph{Contributions} In this context, our typed framework lies upon two main technical contributions:
\begin{enumerate}[(1)]
%\item generalizing the operational semantics of~\cite{DBLP:conf/ppdp/GarraldaCD06}
%so as to account for adaptation in \emph{arbitrary process hierarchies}; 
\item An \emph{operational semantics} for  our session language with located and update processes~\cite{BGPZFMOODS}.
The semantics enables adaptation actions within  \emph{arbitrary process hierarchies} and, following~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
endows each located process with a suitable \emph{runtime annotation}, which describes its active session behavior.
Runtime annotations for locations are key in avoiding undesirable update actions such as the described in~(a) above.

%conservatively extending the typing system in~\cite{DBLP:conf/ppdp/GarraldaCD06}, so as to be able to reason about \emph{process interfaces}.
\item A \emph{typing system} which extends existing session types systems~\cite{DBLP:journals/entcs/YoshidaV07,DBLP:conf/ppdp/GarraldaCD06}
with the notion of \emph{interfaces}, which allow for simple and intuitive static checking rules for evolvability constructs. 
In particular, interfaces are of the essence in avoiding careless updates such as the described in (b) above.
This typing system provides a static analysis technique for ensuring 
\emph{safety}, i.e., absence of communication errors at runtime, but also 
consistency, as described above.
\end{enumerate}

%Ultimately, this last step is what realizes a form of \emph{typeful adaptation}, which contrasts with the untyped adaptation in~\cite{BGPZFMOODS}.  Well-typed processes 
%in our framework
%satisfy basic correctness guarantees (formalized as a Subject Reduction result), 
%which entails consistency for session-typed processes %that
%with runtime adaptation mechanisms.
%
%\jp{Perhaps adding an example of 'wrong' updates/consistency, to be addressed via static analysis?}


%\jp{This paragraph fits better at the end...}



\paragraph{Organization}
%The paper is structured as follows.
Next, in Sect.~\ref{sec:syn}, we present our process language, 
a session calculus with adaptable processes.
In Sect.~\ref{s:types} we present our session type system, and 
in Sect.~\ref{sec:res} we define and investigate its main properties, namely  safety and consistency. 
We illustrate our typed approach via examples in Sect.~\ref{sec:exam}, where we revisit the client/server scenario discussed above.
In Sect.~\ref{sec:int} we discuss extensions and enhancements for typing, in particular refinements for our notion of  interfaces.
Finally, Sect.~\ref{sec:rw} discusses related work and Sect.~\ref{sec:conc} collects some concluding remarks.

This paper is a revised version of the conference paper~\cite{DBLP:conf/sac/GiustoP13}, extended 
with further examples, discussions, as well as with proofs of the main technical results. %\footnote{Process $\adapt{l}{Q}{X}$ was written $l\{Q(\mathsf{X})\}$ in \cite{DBLP:conf/sac/GiustoP13}.}
With respect to~\cite{DBLP:conf/sac/GiustoP13}, in this presentation the operational semantics and typing system
have been much simplified. For instance, while in~\cite{DBLP:conf/sac/GiustoP13} the operational semantics was
instrumented with several elements that supported the static analyses (following~\cite{DBLP:conf/ppdp/GarraldaCD06}), 
the semantics given here is much lighter and relies only on a simple runtime annotation for located processes---the other elements are now subsumed by the (revised) typing discipline. Moreover, Sect.~\ref{ss:examp}, which illustrates runtime adaptation patterns
in an untyped setting, is new to this presentation, whereas 
 Sects.~\ref{sec:exam},~\ref{sec:int}, and~\ref{sec:rw} have been expanded significantly.


